Inference at * 
Iof proof for Lemma equiv rel self functionality:


  T:Type, R:(TT).
  EquivRel(T;x,y.R(x,y))  {a, a', b, b':T. R(a,b)  R(a',b')  (R(a,a')  R(b,b'))} 

latex

 by Unfold `guard` 0 

latex

 1: 

 1:   T:Type, R:(TT).
 1:   EquivRel(T;x,y.R(x,y))  (a, a', b, b':T. R(a,b)  R(a',b')  (R(a,a')  R(b,b')))
 .

Definitions

{T}